1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]3. $T$
\\[0ex]4. $v$ : $T$ List
\\[0ex]5. ${\it bs}$ : $T$ List
\\[0ex]6. nth\_tl($\parallel$$v$$\parallel$;$v$ @ ${\it bs}$) $\sim$ ${\it bs}$
\\[0ex]7. 0 $<$ ($\parallel$$v$$\parallel$+1)
\\[0ex]$\vdash$  (($\parallel$$v$$\parallel$+1) {-} 1) $\sim$ $\parallel$$v$$\parallel$